A:Type, eq:EqDecider(A), B:(AType), f, g:a:A fp B(a). f || g  g || f 

latex

Definitions	P & Q, x:A. B(x), P  Q, t  T, x. t(x), x(s), Top, a:A fp B(a), x  dom(f), b, Prop, f || g, EqDecider(T)
Lemmas	fpf-compatible wf, fpf wf, deq wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top